A, B:Type. finite-type(A)  finite-type(B)  finite-type(A+B) 

latex

Definitions	t  T, x:A. B(x), Prop, (x  l), P & Q, x:A. B(x), P  Q, P  Q, P  Q, finite-type(T), map(f;as), as @ bs, {T}, P  Q
Lemmas	finite-type wf, finite-type-iff-list, append wf, member append, or functionality wrt iff, member map, map wf, l member wf